perm filename FIRST.1[F78,JMC] blob sn#406091 filedate 1978-12-25 generic text, type C, neo UTF8
COMMENT āŠ—   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Introduction and Motivation
C00004 ENDMK
CāŠ—;
Introduction and Motivation

	The study of program correctness has a theoretical aspect
connected with properties of programs and their relations and a
practical aspect connected with developing techniques for proving
actual programs correct.  This paper contains results of both kinds
but is not self-contained with respect to theory, relying heavily
on theorems in the literature, but we hope that the techniques
presented for proving properties of recursive programs are explained
in a self-contained way.  

	The theory of program correctness requires mathematically
motivated people for its development, but its practical use requires
presentations of a cookbook character.  Never mind the proving the
general theorems, tell me how to prove my programs.  This paper
contains results of both kind, but we have attempted to be more
thorough in presenting actual techniques that can be used.

	The practical goal of the theory of program correctness is
that programmers will give machine-checked in